Termination w.r.t. Q proof of TRS/higher-order/LifantsevEx6Folding.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(fold, f), nil), x) → x
app(app(app(fold, f), app(app(cons, h), t)), x) → app(app(app(fold, f), t), app(app(f, x), h))
app(sum, l) → app(app(app(fold, add), l), 0)
app(app(app(fold, mul), l), 1) → app(prod, l)

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(fold, f), nil), x) → x
app(app(app(fold, f), app(app(cons, h), t)), x) → app(app(app(fold, f), t), app(app(f, x), h))
app(sum, l) → app(app(app(fold, add), l), 0)
app(app(app(fold, mul), l), 1) → app(prod, l)

Q is empty.